$\forall$$T$:Type, $R_{1}$,$R_{2}$:($T$$\rightarrow$$T$$\rightarrow$prop\{i:l\}).
\\[0ex]rel\_implies($T$; $R_{1}$; $R_{2}$) $\Rightarrow$ rel\_implies($T$; rel\_plus($T$; $R_{1}$); rel\_plus($T$; $R_{2}$))